$\forall$$T$:Type, $L$:$T$ List, $n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$+1}}$, $x$:$T$. ($x$ $\in$ firstn($n$;$L$)) $\Leftrightarrow$ ($\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$. $x$ $=$ $L$[$i$])